T:Type, c:T, i:Id. constR{x:ut2}(T; c; i)  Realizer 

latex

Definitions	constR{$x:ut2}(T; c; i), Atom$n, Rinit(loc;T;x;v), inl x , x:AB(x), , [car / cdr], Rframe(loc;T;x;L), x:A. B(x), Knd, [], type List, Realizer, "$x", Id, t  T, Type
Lemmas	Id wf, es realizer wf, Knd wf, Rframe wf, rationals wf, Rinit wf, Rlist wf